(set-logic QF_AUFLIA)
(set-info :source |
Benchmarks used in the followin paper:
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
PDPAR'05
http://www.ai.dist.unige.it/pdpar05/


|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun a1 () (Array Int Int))
(declare-fun e1 () Int)
(declare-fun e10 () Int)
(declare-fun e11 () Int)
(declare-fun e12 () Int)
(declare-fun e13 () Int)
(declare-fun e14 () Int)
(declare-fun e15 () Int)
(declare-fun e16 () Int)
(declare-fun e17 () Int)
(declare-fun e18 () Int)
(declare-fun e19 () Int)
(declare-fun e2 () Int)
(declare-fun e20 () Int)
(declare-fun e21 () Int)
(declare-fun e22 () Int)
(declare-fun e23 () Int)
(declare-fun e24 () Int)
(declare-fun e25 () Int)
(declare-fun e26 () Int)
(declare-fun e27 () Int)
(declare-fun e28 () Int)
(declare-fun e29 () Int)
(declare-fun e3 () Int)
(declare-fun e30 () Int)
(declare-fun e31 () Int)
(declare-fun e32 () Int)
(declare-fun e33 () Int)
(declare-fun e34 () Int)
(declare-fun e35 () Int)
(declare-fun e36 () Int)
(declare-fun e37 () Int)
(declare-fun e38 () Int)
(declare-fun e39 () Int)
(declare-fun e4 () Int)
(declare-fun e40 () Int)
(declare-fun e41 () Int)
(declare-fun e42 () Int)
(declare-fun e43 () Int)
(declare-fun e44 () Int)
(declare-fun e45 () Int)
(declare-fun e46 () Int)
(declare-fun e47 () Int)
(declare-fun e48 () Int)
(declare-fun e49 () Int)
(declare-fun e5 () Int)
(declare-fun e50 () Int)
(declare-fun e6 () Int)
(declare-fun e7 () Int)
(declare-fun e8 () Int)
(declare-fun e9 () Int)
(declare-fun i1 () Int)
(declare-fun i10 () Int)
(declare-fun i11 () Int)
(declare-fun i12 () Int)
(declare-fun i13 () Int)
(declare-fun i14 () Int)
(declare-fun i15 () Int)
(declare-fun i16 () Int)
(declare-fun i17 () Int)
(declare-fun i18 () Int)
(declare-fun i19 () Int)
(declare-fun i2 () Int)
(declare-fun i20 () Int)
(declare-fun i21 () Int)
(declare-fun i22 () Int)
(declare-fun i23 () Int)
(declare-fun i24 () Int)
(declare-fun i25 () Int)
(declare-fun i26 () Int)
(declare-fun i27 () Int)
(declare-fun i28 () Int)
(declare-fun i29 () Int)
(declare-fun i3 () Int)
(declare-fun i30 () Int)
(declare-fun i31 () Int)
(declare-fun i32 () Int)
(declare-fun i33 () Int)
(declare-fun i34 () Int)
(declare-fun i35 () Int)
(declare-fun i36 () Int)
(declare-fun i37 () Int)
(declare-fun i38 () Int)
(declare-fun i39 () Int)
(declare-fun i4 () Int)
(declare-fun i40 () Int)
(declare-fun i41 () Int)
(declare-fun i42 () Int)
(declare-fun i43 () Int)
(declare-fun i44 () Int)
(declare-fun i45 () Int)
(declare-fun i46 () Int)
(declare-fun i47 () Int)
(declare-fun i48 () Int)
(declare-fun i49 () Int)
(declare-fun i5 () Int)
(declare-fun i50 () Int)
(declare-fun i6 () Int)
(declare-fun i7 () Int)
(declare-fun i8 () Int)
(declare-fun i9 () Int)
(declare-fun sk ((Array Int Int) (Array Int Int)) Int)
(assert (not (= i49 i50)))
(assert (not (= i48 i50)))
(assert (not (= i48 i49)))
(assert (not (= i47 i50)))
(assert (not (= i47 i49)))
(assert (not (= i47 i48)))
(assert (not (= i46 i50)))
(assert (not (= i46 i49)))
(assert (not (= i46 i48)))
(assert (not (= i46 i47)))
(assert (not (= i45 i50)))
(assert (not (= i45 i49)))
(assert (not (= i45 i48)))
(assert (not (= i45 i47)))
(assert (not (= i45 i46)))
(assert (not (= i44 i50)))
(assert (not (= i44 i49)))
(assert (not (= i44 i48)))
(assert (not (= i44 i47)))
(assert (not (= i44 i46)))
(assert (not (= i44 i45)))
(assert (not (= i43 i50)))
(assert (not (= i43 i49)))
(assert (not (= i43 i48)))
(assert (not (= i43 i47)))
(assert (not (= i43 i46)))
(assert (not (= i43 i45)))
(assert (not (= i43 i44)))
(assert (not (= i42 i50)))
(assert (not (= i42 i49)))
(assert (not (= i42 i48)))
(assert (not (= i42 i47)))
(assert (not (= i42 i46)))
(assert (not (= i42 i45)))
(assert (not (= i42 i44)))
(assert (not (= i42 i43)))
(assert (not (= i41 i50)))
(assert (not (= i41 i49)))
(assert (not (= i41 i48)))
(assert (not (= i41 i47)))
(assert (not (= i41 i46)))
(assert (not (= i41 i45)))
(assert (not (= i41 i44)))
(assert (not (= i41 i43)))
(assert (not (= i41 i42)))
(assert (not (= i40 i50)))
(assert (not (= i40 i49)))
(assert (not (= i40 i48)))
(assert (not (= i40 i47)))
(assert (not (= i40 i46)))
(assert (not (= i40 i45)))
(assert (not (= i40 i44)))
(assert (not (= i40 i43)))
(assert (not (= i40 i42)))
(assert (not (= i40 i41)))
(assert (not (= i39 i50)))
(assert (not (= i39 i49)))
(assert (not (= i39 i48)))
(assert (not (= i39 i47)))
(assert (not (= i39 i46)))
(assert (not (= i39 i45)))
(assert (not (= i39 i44)))
(assert (not (= i39 i43)))
(assert (not (= i39 i42)))
(assert (not (= i39 i41)))
(assert (not (= i39 i40)))
(assert (not (= i38 i50)))
(assert (not (= i38 i49)))
(assert (not (= i38 i48)))
(assert (not (= i38 i47)))
(assert (not (= i38 i46)))
(assert (not (= i38 i45)))
(assert (not (= i38 i44)))
(assert (not (= i38 i43)))
(assert (not (= i38 i42)))
(assert (not (= i38 i41)))
(assert (not (= i38 i40)))
(assert (not (= i38 i39)))
(assert (not (= i37 i50)))
(assert (not (= i37 i49)))
(assert (not (= i37 i48)))
(assert (not (= i37 i47)))
(assert (not (= i37 i46)))
(assert (not (= i37 i45)))
(assert (not (= i37 i44)))
(assert (not (= i37 i43)))
(assert (not (= i37 i42)))
(assert (not (= i37 i41)))
(assert (not (= i37 i40)))
(assert (not (= i37 i39)))
(assert (not (= i37 i38)))
(assert (not (= i36 i50)))
(assert (not (= i36 i49)))
(assert (not (= i36 i48)))
(assert (not (= i36 i47)))
(assert (not (= i36 i46)))
(assert (not (= i36 i45)))
(assert (not (= i36 i44)))
(assert (not (= i36 i43)))
(assert (not (= i36 i42)))
(assert (not (= i36 i41)))
(assert (not (= i36 i40)))
(assert (not (= i36 i39)))
(assert (not (= i36 i38)))
(assert (not (= i36 i37)))
(assert (not (= i35 i50)))
(assert (not (= i35 i49)))
(assert (not (= i35 i48)))
(assert (not (= i35 i47)))
(assert (not (= i35 i46)))
(assert (not (= i35 i45)))
(assert (not (= i35 i44)))
(assert (not (= i35 i43)))
(assert (not (= i35 i42)))
(assert (not (= i35 i41)))
(assert (not (= i35 i40)))
(assert (not (= i35 i39)))
(assert (not (= i35 i38)))
(assert (not (= i35 i37)))
(assert (not (= i35 i36)))
(assert (not (= i34 i50)))
(assert (not (= i34 i49)))
(assert (not (= i34 i48)))
(assert (not (= i34 i47)))
(assert (not (= i34 i46)))
(assert (not (= i34 i45)))
(assert (not (= i34 i44)))
(assert (not (= i34 i43)))
(assert (not (= i34 i42)))
(assert (not (= i34 i41)))
(assert (not (= i34 i40)))
(assert (not (= i34 i39)))
(assert (not (= i34 i38)))
(assert (not (= i34 i37)))
(assert (not (= i34 i36)))
(assert (not (= i34 i35)))
(assert (not (= i33 i50)))
(assert (not (= i33 i49)))
(assert (not (= i33 i48)))
(assert (not (= i33 i47)))
(assert (not (= i33 i46)))
(assert (not (= i33 i45)))
(assert (not (= i33 i44)))
(assert (not (= i33 i43)))
(assert (not (= i33 i42)))
(assert (not (= i33 i41)))
(assert (not (= i33 i40)))
(assert (not (= i33 i39)))
(assert (not (= i33 i38)))
(assert (not (= i33 i37)))
(assert (not (= i33 i36)))
(assert (not (= i33 i35)))
(assert (not (= i33 i34)))
(assert (not (= i32 i50)))
(assert (not (= i32 i49)))
(assert (not (= i32 i48)))
(assert (not (= i32 i47)))
(assert (not (= i32 i46)))
(assert (not (= i32 i45)))
(assert (not (= i32 i44)))
(assert (not (= i32 i43)))
(assert (not (= i32 i42)))
(assert (not (= i32 i41)))
(assert (not (= i32 i40)))
(assert (not (= i32 i39)))
(assert (not (= i32 i38)))
(assert (not (= i32 i37)))
(assert (not (= i32 i36)))
(assert (not (= i32 i35)))
(assert (not (= i32 i34)))
(assert (not (= i32 i33)))
(assert (not (= i31 i50)))
(assert (not (= i31 i49)))
(assert (not (= i31 i48)))
(assert (not (= i31 i47)))
(assert (not (= i31 i46)))
(assert (not (= i31 i45)))
(assert (not (= i31 i44)))
(assert (not (= i31 i43)))
(assert (not (= i31 i42)))
(assert (not (= i31 i41)))
(assert (not (= i31 i40)))
(assert (not (= i31 i39)))
(assert (not (= i31 i38)))
(assert (not (= i31 i37)))
(assert (not (= i31 i36)))
(assert (not (= i31 i35)))
(assert (not (= i31 i34)))
(assert (not (= i31 i33)))
(assert (not (= i31 i32)))
(assert (not (= i30 i50)))
(assert (not (= i30 i49)))
(assert (not (= i30 i48)))
(assert (not (= i30 i47)))
(assert (not (= i30 i46)))
(assert (not (= i30 i45)))
(assert (not (= i30 i44)))
(assert (not (= i30 i43)))
(assert (not (= i30 i42)))
(assert (not (= i30 i41)))
(assert (not (= i30 i40)))
(assert (not (= i30 i39)))
(assert (not (= i30 i38)))
(assert (not (= i30 i37)))
(assert (not (= i30 i36)))
(assert (not (= i30 i35)))
(assert (not (= i30 i34)))
(assert (not (= i30 i33)))
(assert (not (= i30 i32)))
(assert (not (= i30 i31)))
(assert (not (= i29 i50)))
(assert (not (= i29 i49)))
(assert (not (= i29 i48)))
(assert (not (= i29 i47)))
(assert (not (= i29 i46)))
(assert (not (= i29 i45)))
(assert (not (= i29 i44)))
(assert (not (= i29 i43)))
(assert (not (= i29 i42)))
(assert (not (= i29 i41)))
(assert (not (= i29 i40)))
(assert (not (= i29 i39)))
(assert (not (= i29 i38)))
(assert (not (= i29 i37)))
(assert (not (= i29 i36)))
(assert (not (= i29 i35)))
(assert (not (= i29 i34)))
(assert (not (= i29 i33)))
(assert (not (= i29 i32)))
(assert (not (= i29 i31)))
(assert (not (= i29 i30)))
(assert (not (= i28 i50)))
(assert (not (= i28 i49)))
(assert (not (= i28 i48)))
(assert (not (= i28 i47)))
(assert (not (= i28 i46)))
(assert (not (= i28 i45)))
(assert (not (= i28 i44)))
(assert (not (= i28 i43)))
(assert (not (= i28 i42)))
(assert (not (= i28 i41)))
(assert (not (= i28 i40)))
(assert (not (= i28 i39)))
(assert (not (= i28 i38)))
(assert (not (= i28 i37)))
(assert (not (= i28 i36)))
(assert (not (= i28 i35)))
(assert (not (= i28 i34)))
(assert (not (= i28 i33)))
(assert (not (= i28 i32)))
(assert (not (= i28 i31)))
(assert (not (= i28 i30)))
(assert (not (= i28 i29)))
(assert (not (= i27 i50)))
(assert (not (= i27 i49)))
(assert (not (= i27 i48)))
(assert (not (= i27 i47)))
(assert (not (= i27 i46)))
(assert (not (= i27 i45)))
(assert (not (= i27 i44)))
(assert (not (= i27 i43)))
(assert (not (= i27 i42)))
(assert (not (= i27 i41)))
(assert (not (= i27 i40)))
(assert (not (= i27 i39)))
(assert (not (= i27 i38)))
(assert (not (= i27 i37)))
(assert (not (= i27 i36)))
(assert (not (= i27 i35)))
(assert (not (= i27 i34)))
(assert (not (= i27 i33)))
(assert (not (= i27 i32)))
(assert (not (= i27 i31)))
(assert (not (= i27 i30)))
(assert (not (= i27 i29)))
(assert (not (= i27 i28)))
(assert (not (= i26 i50)))
(assert (not (= i26 i49)))
(assert (not (= i26 i48)))
(assert (not (= i26 i47)))
(assert (not (= i26 i46)))
(assert (not (= i26 i45)))
(assert (not (= i26 i44)))
(assert (not (= i26 i43)))
(assert (not (= i26 i42)))
(assert (not (= i26 i41)))
(assert (not (= i26 i40)))
(assert (not (= i26 i39)))
(assert (not (= i26 i38)))
(assert (not (= i26 i37)))
(assert (not (= i26 i36)))
(assert (not (= i26 i35)))
(assert (not (= i26 i34)))
(assert (not (= i26 i33)))
(assert (not (= i26 i32)))
(assert (not (= i26 i31)))
(assert (not (= i26 i30)))
(assert (not (= i26 i29)))
(assert (not (= i26 i28)))
(assert (not (= i26 i27)))
(assert (not (= i25 i50)))
(assert (not (= i25 i49)))
(assert (not (= i25 i48)))
(assert (not (= i25 i47)))
(assert (not (= i25 i46)))
(assert (not (= i25 i45)))
(assert (not (= i25 i44)))
(assert (not (= i25 i43)))
(assert (not (= i25 i42)))
(assert (not (= i25 i41)))
(assert (not (= i25 i40)))
(assert (not (= i25 i39)))
(assert (not (= i25 i38)))
(assert (not (= i25 i37)))
(assert (not (= i25 i36)))
(assert (not (= i25 i35)))
(assert (not (= i25 i34)))
(assert (not (= i25 i33)))
(assert (not (= i25 i32)))
(assert (not (= i25 i31)))
(assert (not (= i25 i30)))
(assert (not (= i25 i29)))
(assert (not (= i25 i28)))
(assert (not (= i25 i27)))
(assert (not (= i25 i26)))
(assert (not (= i24 i50)))
(assert (not (= i24 i49)))
(assert (not (= i24 i48)))
(assert (not (= i24 i47)))
(assert (not (= i24 i46)))
(assert (not (= i24 i45)))
(assert (not (= i24 i44)))
(assert (not (= i24 i43)))
(assert (not (= i24 i42)))
(assert (not (= i24 i41)))
(assert (not (= i24 i40)))
(assert (not (= i24 i39)))
(assert (not (= i24 i38)))
(assert (not (= i24 i37)))
(assert (not (= i24 i36)))
(assert (not (= i24 i35)))
(assert (not (= i24 i34)))
(assert (not (= i24 i33)))
(assert (not (= i24 i32)))
(assert (not (= i24 i31)))
(assert (not (= i24 i30)))
(assert (not (= i24 i29)))
(assert (not (= i24 i28)))
(assert (not (= i24 i27)))
(assert (not (= i24 i26)))
(assert (not (= i24 i25)))
(assert (not (= i23 i50)))
(assert (not (= i23 i49)))
(assert (not (= i23 i48)))
(assert (not (= i23 i47)))
(assert (not (= i23 i46)))
(assert (not (= i23 i45)))
(assert (not (= i23 i44)))
(assert (not (= i23 i43)))
(assert (not (= i23 i42)))
(assert (not (= i23 i41)))
(assert (not (= i23 i40)))
(assert (not (= i23 i39)))
(assert (not (= i23 i38)))
(assert (not (= i23 i37)))
(assert (not (= i23 i36)))
(assert (not (= i23 i35)))
(assert (not (= i23 i34)))
(assert (not (= i23 i33)))
(assert (not (= i23 i32)))
(assert (not (= i23 i31)))
(assert (not (= i23 i30)))
(assert (not (= i23 i29)))
(assert (not (= i23 i28)))
(assert (not (= i23 i27)))
(assert (not (= i23 i26)))
(assert (not (= i23 i25)))
(assert (not (= i23 i24)))
(assert (not (= i22 i50)))
(assert (not (= i22 i49)))
(assert (not (= i22 i48)))
(assert (not (= i22 i47)))
(assert (not (= i22 i46)))
(assert (not (= i22 i45)))
(assert (not (= i22 i44)))
(assert (not (= i22 i43)))
(assert (not (= i22 i42)))
(assert (not (= i22 i41)))
(assert (not (= i22 i40)))
(assert (not (= i22 i39)))
(assert (not (= i22 i38)))
(assert (not (= i22 i37)))
(assert (not (= i22 i36)))
(assert (not (= i22 i35)))
(assert (not (= i22 i34)))
(assert (not (= i22 i33)))
(assert (not (= i22 i32)))
(assert (not (= i22 i31)))
(assert (not (= i22 i30)))
(assert (not (= i22 i29)))
(assert (not (= i22 i28)))
(assert (not (= i22 i27)))
(assert (not (= i22 i26)))
(assert (not (= i22 i25)))
(assert (not (= i22 i24)))
(assert (not (= i22 i23)))
(assert (not (= i21 i50)))
(assert (not (= i21 i49)))
(assert (not (= i21 i48)))
(assert (not (= i21 i47)))
(assert (not (= i21 i46)))
(assert (not (= i21 i45)))
(assert (not (= i21 i44)))
(assert (not (= i21 i43)))
(assert (not (= i21 i42)))
(assert (not (= i21 i41)))
(assert (not (= i21 i40)))
(assert (not (= i21 i39)))
(assert (not (= i21 i38)))
(assert (not (= i21 i37)))
(assert (not (= i21 i36)))
(assert (not (= i21 i35)))
(assert (not (= i21 i34)))
(assert (not (= i21 i33)))
(assert (not (= i21 i32)))
(assert (not (= i21 i31)))
(assert (not (= i21 i30)))
(assert (not (= i21 i29)))
(assert (not (= i21 i28)))
(assert (not (= i21 i27)))
(assert (not (= i21 i26)))
(assert (not (= i21 i25)))
(assert (not (= i21 i24)))
(assert (not (= i21 i23)))
(assert (not (= i21 i22)))
(assert (not (= i20 i50)))
(assert (not (= i20 i49)))
(assert (not (= i20 i48)))
(assert (not (= i20 i47)))
(assert (not (= i20 i46)))
(assert (not (= i20 i45)))
(assert (not (= i20 i44)))
(assert (not (= i20 i43)))
(assert (not (= i20 i42)))
(assert (not (= i20 i41)))
(assert (not (= i20 i40)))
(assert (not (= i20 i39)))
(assert (not (= i20 i38)))
(assert (not (= i20 i37)))
(assert (not (= i20 i36)))
(assert (not (= i20 i35)))
(assert (not (= i20 i34)))
(assert (not (= i20 i33)))
(assert (not (= i20 i32)))
(assert (not (= i20 i31)))
(assert (not (= i20 i30)))
(assert (not (= i20 i29)))
(assert (not (= i20 i28)))
(assert (not (= i20 i27)))
(assert (not (= i20 i26)))
(assert (not (= i20 i25)))
(assert (not (= i20 i24)))
(assert (not (= i20 i23)))
(assert (not (= i20 i22)))
(assert (not (= i20 i21)))
(assert (not (= i19 i50)))
(assert (not (= i19 i49)))
(assert (not (= i19 i48)))
(assert (not (= i19 i47)))
(assert (not (= i19 i46)))
(assert (not (= i19 i45)))
(assert (not (= i19 i44)))
(assert (not (= i19 i43)))
(assert (not (= i19 i42)))
(assert (not (= i19 i41)))
(assert (not (= i19 i40)))
(assert (not (= i19 i39)))
(assert (not (= i19 i38)))
(assert (not (= i19 i37)))
(assert (not (= i19 i36)))
(assert (not (= i19 i35)))
(assert (not (= i19 i34)))
(assert (not (= i19 i33)))
(assert (not (= i19 i32)))
(assert (not (= i19 i31)))
(assert (not (= i19 i30)))
(assert (not (= i19 i29)))
(assert (not (= i19 i28)))
(assert (not (= i19 i27)))
(assert (not (= i19 i26)))
(assert (not (= i19 i25)))
(assert (not (= i19 i24)))
(assert (not (= i19 i23)))
(assert (not (= i19 i22)))
(assert (not (= i19 i21)))
(assert (not (= i19 i20)))
(assert (not (= i18 i50)))
(assert (not (= i18 i49)))
(assert (not (= i18 i48)))
(assert (not (= i18 i47)))
(assert (not (= i18 i46)))
(assert (not (= i18 i45)))
(assert (not (= i18 i44)))
(assert (not (= i18 i43)))
(assert (not (= i18 i42)))
(assert (not (= i18 i41)))
(assert (not (= i18 i40)))
(assert (not (= i18 i39)))
(assert (not (= i18 i38)))
(assert (not (= i18 i37)))
(assert (not (= i18 i36)))
(assert (not (= i18 i35)))
(assert (not (= i18 i34)))
(assert (not (= i18 i33)))
(assert (not (= i18 i32)))
(assert (not (= i18 i31)))
(assert (not (= i18 i30)))
(assert (not (= i18 i29)))
(assert (not (= i18 i28)))
(assert (not (= i18 i27)))
(assert (not (= i18 i26)))
(assert (not (= i18 i25)))
(assert (not (= i18 i24)))
(assert (not (= i18 i23)))
(assert (not (= i18 i22)))
(assert (not (= i18 i21)))
(assert (not (= i18 i20)))
(assert (not (= i18 i19)))
(assert (not (= i17 i50)))
(assert (not (= i17 i49)))
(assert (not (= i17 i48)))
(assert (not (= i17 i47)))
(assert (not (= i17 i46)))
(assert (not (= i17 i45)))
(assert (not (= i17 i44)))
(assert (not (= i17 i43)))
(assert (not (= i17 i42)))
(assert (not (= i17 i41)))
(assert (not (= i17 i40)))
(assert (not (= i17 i39)))
(assert (not (= i17 i38)))
(assert (not (= i17 i37)))
(assert (not (= i17 i36)))
(assert (not (= i17 i35)))
(assert (not (= i17 i34)))
(assert (not (= i17 i33)))
(assert (not (= i17 i32)))
(assert (not (= i17 i31)))
(assert (not (= i17 i30)))
(assert (not (= i17 i29)))
(assert (not (= i17 i28)))
(assert (not (= i17 i27)))
(assert (not (= i17 i26)))
(assert (not (= i17 i25)))
(assert (not (= i17 i24)))
(assert (not (= i17 i23)))
(assert (not (= i17 i22)))
(assert (not (= i17 i21)))
(assert (not (= i17 i20)))
(assert (not (= i17 i19)))
(assert (not (= i17 i18)))
(assert (not (= i16 i50)))
(assert (not (= i16 i49)))
(assert (not (= i16 i48)))
(assert (not (= i16 i47)))
(assert (not (= i16 i46)))
(assert (not (= i16 i45)))
(assert (not (= i16 i44)))
(assert (not (= i16 i43)))
(assert (not (= i16 i42)))
(assert (not (= i16 i41)))
(assert (not (= i16 i40)))
(assert (not (= i16 i39)))
(assert (not (= i16 i38)))
(assert (not (= i16 i37)))
(assert (not (= i16 i36)))
(assert (not (= i16 i35)))
(assert (not (= i16 i34)))
(assert (not (= i16 i33)))
(assert (not (= i16 i32)))
(assert (not (= i16 i31)))
(assert (not (= i16 i30)))
(assert (not (= i16 i29)))
(assert (not (= i16 i28)))
(assert (not (= i16 i27)))
(assert (not (= i16 i26)))
(assert (not (= i16 i25)))
(assert (not (= i16 i24)))
(assert (not (= i16 i23)))
(assert (not (= i16 i22)))
(assert (not (= i16 i21)))
(assert (not (= i16 i20)))
(assert (not (= i16 i19)))
(assert (not (= i16 i18)))
(assert (not (= i16 i17)))
(assert (not (= i15 i50)))
(assert (not (= i15 i49)))
(assert (not (= i15 i48)))
(assert (not (= i15 i47)))
(assert (not (= i15 i46)))
(assert (not (= i15 i45)))
(assert (not (= i15 i44)))
(assert (not (= i15 i43)))
(assert (not (= i15 i42)))
(assert (not (= i15 i41)))
(assert (not (= i15 i40)))
(assert (not (= i15 i39)))
(assert (not (= i15 i38)))
(assert (not (= i15 i37)))
(assert (not (= i15 i36)))
(assert (not (= i15 i35)))
(assert (not (= i15 i34)))
(assert (not (= i15 i33)))
(assert (not (= i15 i32)))
(assert (not (= i15 i31)))
(assert (not (= i15 i30)))
(assert (not (= i15 i29)))
(assert (not (= i15 i28)))
(assert (not (= i15 i27)))
(assert (not (= i15 i26)))
(assert (not (= i15 i25)))
(assert (not (= i15 i24)))
(assert (not (= i15 i23)))
(assert (not (= i15 i22)))
(assert (not (= i15 i21)))
(assert (not (= i15 i20)))
(assert (not (= i15 i19)))
(assert (not (= i15 i18)))
(assert (not (= i15 i17)))
(assert (not (= i15 i16)))
(assert (not (= i14 i50)))
(assert (not (= i14 i49)))
(assert (not (= i14 i48)))
(assert (not (= i14 i47)))
(assert (not (= i14 i46)))
(assert (not (= i14 i45)))
(assert (not (= i14 i44)))
(assert (not (= i14 i43)))
(assert (not (= i14 i42)))
(assert (not (= i14 i41)))
(assert (not (= i14 i40)))
(assert (not (= i14 i39)))
(assert (not (= i14 i38)))
(assert (not (= i14 i37)))
(assert (not (= i14 i36)))
(assert (not (= i14 i35)))
(assert (not (= i14 i34)))
(assert (not (= i14 i33)))
(assert (not (= i14 i32)))
(assert (not (= i14 i31)))
(assert (not (= i14 i30)))
(assert (not (= i14 i29)))
(assert (not (= i14 i28)))
(assert (not (= i14 i27)))
(assert (not (= i14 i26)))
(assert (not (= i14 i25)))
(assert (not (= i14 i24)))
(assert (not (= i14 i23)))
(assert (not (= i14 i22)))
(assert (not (= i14 i21)))
(assert (not (= i14 i20)))
(assert (not (= i14 i19)))
(assert (not (= i14 i18)))
(assert (not (= i14 i17)))
(assert (not (= i14 i16)))
(assert (not (= i14 i15)))
(assert (not (= i13 i50)))
(assert (not (= i13 i49)))
(assert (not (= i13 i48)))
(assert (not (= i13 i47)))
(assert (not (= i13 i46)))
(assert (not (= i13 i45)))
(assert (not (= i13 i44)))
(assert (not (= i13 i43)))
(assert (not (= i13 i42)))
(assert (not (= i13 i41)))
(assert (not (= i13 i40)))
(assert (not (= i13 i39)))
(assert (not (= i13 i38)))
(assert (not (= i13 i37)))
(assert (not (= i13 i36)))
(assert (not (= i13 i35)))
(assert (not (= i13 i34)))
(assert (not (= i13 i33)))
(assert (not (= i13 i32)))
(assert (not (= i13 i31)))
(assert (not (= i13 i30)))
(assert (not (= i13 i29)))
(assert (not (= i13 i28)))
(assert (not (= i13 i27)))
(assert (not (= i13 i26)))
(assert (not (= i13 i25)))
(assert (not (= i13 i24)))
(assert (not (= i13 i23)))
(assert (not (= i13 i22)))
(assert (not (= i13 i21)))
(assert (not (= i13 i20)))
(assert (not (= i13 i19)))
(assert (not (= i13 i18)))
(assert (not (= i13 i17)))
(assert (not (= i13 i16)))
(assert (not (= i13 i15)))
(assert (not (= i13 i14)))
(assert (not (= i12 i50)))
(assert (not (= i12 i49)))
(assert (not (= i12 i48)))
(assert (not (= i12 i47)))
(assert (not (= i12 i46)))
(assert (not (= i12 i45)))
(assert (not (= i12 i44)))
(assert (not (= i12 i43)))
(assert (not (= i12 i42)))
(assert (not (= i12 i41)))
(assert (not (= i12 i40)))
(assert (not (= i12 i39)))
(assert (not (= i12 i38)))
(assert (not (= i12 i37)))
(assert (not (= i12 i36)))
(assert (not (= i12 i35)))
(assert (not (= i12 i34)))
(assert (not (= i12 i33)))
(assert (not (= i12 i32)))
(assert (not (= i12 i31)))
(assert (not (= i12 i30)))
(assert (not (= i12 i29)))
(assert (not (= i12 i28)))
(assert (not (= i12 i27)))
(assert (not (= i12 i26)))
(assert (not (= i12 i25)))
(assert (not (= i12 i24)))
(assert (not (= i12 i23)))
(assert (not (= i12 i22)))
(assert (not (= i12 i21)))
(assert (not (= i12 i20)))
(assert (not (= i12 i19)))
(assert (not (= i12 i18)))
(assert (not (= i12 i17)))
(assert (not (= i12 i16)))
(assert (not (= i12 i15)))
(assert (not (= i12 i14)))
(assert (not (= i12 i13)))
(assert (not (= i11 i50)))
(assert (not (= i11 i49)))
(assert (not (= i11 i48)))
(assert (not (= i11 i47)))
(assert (not (= i11 i46)))
(assert (not (= i11 i45)))
(assert (not (= i11 i44)))
(assert (not (= i11 i43)))
(assert (not (= i11 i42)))
(assert (not (= i11 i41)))
(assert (not (= i11 i40)))
(assert (not (= i11 i39)))
(assert (not (= i11 i38)))
(assert (not (= i11 i37)))
(assert (not (= i11 i36)))
(assert (not (= i11 i35)))
(assert (not (= i11 i34)))
(assert (not (= i11 i33)))
(assert (not (= i11 i32)))
(assert (not (= i11 i31)))
(assert (not (= i11 i30)))
(assert (not (= i11 i29)))
(assert (not (= i11 i28)))
(assert (not (= i11 i27)))
(assert (not (= i11 i26)))
(assert (not (= i11 i25)))
(assert (not (= i11 i24)))
(assert (not (= i11 i23)))
(assert (not (= i11 i22)))
(assert (not (= i11 i21)))
(assert (not (= i11 i20)))
(assert (not (= i11 i19)))
(assert (not (= i11 i18)))
(assert (not (= i11 i17)))
(assert (not (= i11 i16)))
(assert (not (= i11 i15)))
(assert (not (= i11 i14)))
(assert (not (= i11 i13)))
(assert (not (= i11 i12)))
(assert (not (= i10 i50)))
(assert (not (= i10 i49)))
(assert (not (= i10 i48)))
(assert (not (= i10 i47)))
(assert (not (= i10 i46)))
(assert (not (= i10 i45)))
(assert (not (= i10 i44)))
(assert (not (= i10 i43)))
(assert (not (= i10 i42)))
(assert (not (= i10 i41)))
(assert (not (= i10 i40)))
(assert (not (= i10 i39)))
(assert (not (= i10 i38)))
(assert (not (= i10 i37)))
(assert (not (= i10 i36)))
(assert (not (= i10 i35)))
(assert (not (= i10 i34)))
(assert (not (= i10 i33)))
(assert (not (= i10 i32)))
(assert (not (= i10 i31)))
(assert (not (= i10 i30)))
(assert (not (= i10 i29)))
(assert (not (= i10 i28)))
(assert (not (= i10 i27)))
(assert (not (= i10 i26)))
(assert (not (= i10 i25)))
(assert (not (= i10 i24)))
(assert (not (= i10 i23)))
(assert (not (= i10 i22)))
(assert (not (= i10 i21)))
(assert (not (= i10 i20)))
(assert (not (= i10 i19)))
(assert (not (= i10 i18)))
(assert (not (= i10 i17)))
(assert (not (= i10 i16)))
(assert (not (= i10 i15)))
(assert (not (= i10 i14)))
(assert (not (= i10 i13)))
(assert (not (= i10 i12)))
(assert (not (= i10 i11)))
(assert (not (= i9 i50)))
(assert (not (= i9 i49)))
(assert (not (= i9 i48)))
(assert (not (= i9 i47)))
(assert (not (= i9 i46)))
(assert (not (= i9 i45)))
(assert (not (= i9 i44)))
(assert (not (= i9 i43)))
(assert (not (= i9 i42)))
(assert (not (= i9 i41)))
(assert (not (= i9 i40)))
(assert (not (= i9 i39)))
(assert (not (= i9 i38)))
(assert (not (= i9 i37)))
(assert (not (= i9 i36)))
(assert (not (= i9 i35)))
(assert (not (= i9 i34)))
(assert (not (= i9 i33)))
(assert (not (= i9 i32)))
(assert (not (= i9 i31)))
(assert (not (= i9 i30)))
(assert (not (= i9 i29)))
(assert (not (= i9 i28)))
(assert (not (= i9 i27)))
(assert (not (= i9 i26)))
(assert (not (= i9 i25)))
(assert (not (= i9 i24)))
(assert (not (= i9 i23)))
(assert (not (= i9 i22)))
(assert (not (= i9 i21)))
(assert (not (= i9 i20)))
(assert (not (= i9 i19)))
(assert (not (= i9 i18)))
(assert (not (= i9 i17)))
(assert (not (= i9 i16)))
(assert (not (= i9 i15)))
(assert (not (= i9 i14)))
(assert (not (= i9 i13)))
(assert (not (= i9 i12)))
(assert (not (= i9 i11)))
(assert (not (= i9 i10)))
(assert (not (= i8 i50)))
(assert (not (= i8 i49)))
(assert (not (= i8 i48)))
(assert (not (= i8 i47)))
(assert (not (= i8 i46)))
(assert (not (= i8 i45)))
(assert (not (= i8 i44)))
(assert (not (= i8 i43)))
(assert (not (= i8 i42)))
(assert (not (= i8 i41)))
(assert (not (= i8 i40)))
(assert (not (= i8 i39)))
(assert (not (= i8 i38)))
(assert (not (= i8 i37)))
(assert (not (= i8 i36)))
(assert (not (= i8 i35)))
(assert (not (= i8 i34)))
(assert (not (= i8 i33)))
(assert (not (= i8 i32)))
(assert (not (= i8 i31)))
(assert (not (= i8 i30)))
(assert (not (= i8 i29)))
(assert (not (= i8 i28)))
(assert (not (= i8 i27)))
(assert (not (= i8 i26)))
(assert (not (= i8 i25)))
(assert (not (= i8 i24)))
(assert (not (= i8 i23)))
(assert (not (= i8 i22)))
(assert (not (= i8 i21)))
(assert (not (= i8 i20)))
(assert (not (= i8 i19)))
(assert (not (= i8 i18)))
(assert (not (= i8 i17)))
(assert (not (= i8 i16)))
(assert (not (= i8 i15)))
(assert (not (= i8 i14)))
(assert (not (= i8 i13)))
(assert (not (= i8 i12)))
(assert (not (= i8 i11)))
(assert (not (= i8 i10)))
(assert (not (= i8 i9)))
(assert (not (= i7 i50)))
(assert (not (= i7 i49)))
(assert (not (= i7 i48)))
(assert (not (= i7 i47)))
(assert (not (= i7 i46)))
(assert (not (= i7 i45)))
(assert (not (= i7 i44)))
(assert (not (= i7 i43)))
(assert (not (= i7 i42)))
(assert (not (= i7 i41)))
(assert (not (= i7 i40)))
(assert (not (= i7 i39)))
(assert (not (= i7 i38)))
(assert (not (= i7 i37)))
(assert (not (= i7 i36)))
(assert (not (= i7 i35)))
(assert (not (= i7 i34)))
(assert (not (= i7 i33)))
(assert (not (= i7 i32)))
(assert (not (= i7 i31)))
(assert (not (= i7 i30)))
(assert (not (= i7 i29)))
(assert (not (= i7 i28)))
(assert (not (= i7 i27)))
(assert (not (= i7 i26)))
(assert (not (= i7 i25)))
(assert (not (= i7 i24)))
(assert (not (= i7 i23)))
(assert (not (= i7 i22)))
(assert (not (= i7 i21)))
(assert (not (= i7 i20)))
(assert (not (= i7 i19)))
(assert (not (= i7 i18)))
(assert (not (= i7 i17)))
(assert (not (= i7 i16)))
(assert (not (= i7 i15)))
(assert (not (= i7 i14)))
(assert (not (= i7 i13)))
(assert (not (= i7 i12)))
(assert (not (= i7 i11)))
(assert (not (= i7 i10)))
(assert (not (= i7 i9)))
(assert (not (= i7 i8)))
(assert (not (= i6 i50)))
(assert (not (= i6 i49)))
(assert (not (= i6 i48)))
(assert (not (= i6 i47)))
(assert (not (= i6 i46)))
(assert (not (= i6 i45)))
(assert (not (= i6 i44)))
(assert (not (= i6 i43)))
(assert (not (= i6 i42)))
(assert (not (= i6 i41)))
(assert (not (= i6 i40)))
(assert (not (= i6 i39)))
(assert (not (= i6 i38)))
(assert (not (= i6 i37)))
(assert (not (= i6 i36)))
(assert (not (= i6 i35)))
(assert (not (= i6 i34)))
(assert (not (= i6 i33)))
(assert (not (= i6 i32)))
(assert (not (= i6 i31)))
(assert (not (= i6 i30)))
(assert (not (= i6 i29)))
(assert (not (= i6 i28)))
(assert (not (= i6 i27)))
(assert (not (= i6 i26)))
(assert (not (= i6 i25)))
(assert (not (= i6 i24)))
(assert (not (= i6 i23)))
(assert (not (= i6 i22)))
(assert (not (= i6 i21)))
(assert (not (= i6 i20)))
(assert (not (= i6 i19)))
(assert (not (= i6 i18)))
(assert (not (= i6 i17)))
(assert (not (= i6 i16)))
(assert (not (= i6 i15)))
(assert (not (= i6 i14)))
(assert (not (= i6 i13)))
(assert (not (= i6 i12)))
(assert (not (= i6 i11)))
(assert (not (= i6 i10)))
(assert (not (= i6 i9)))
(assert (not (= i6 i8)))
(assert (not (= i6 i7)))
(assert (not (= i5 i50)))
(assert (not (= i5 i49)))
(assert (not (= i5 i48)))
(assert (not (= i5 i47)))
(assert (not (= i5 i46)))
(assert (not (= i5 i45)))
(assert (not (= i5 i44)))
(assert (not (= i5 i43)))
(assert (not (= i5 i42)))
(assert (not (= i5 i41)))
(assert (not (= i5 i40)))
(assert (not (= i5 i39)))
(assert (not (= i5 i38)))
(assert (not (= i5 i37)))
(assert (not (= i5 i36)))
(assert (not (= i5 i35)))
(assert (not (= i5 i34)))
(assert (not (= i5 i33)))
(assert (not (= i5 i32)))
(assert (not (= i5 i31)))
(assert (not (= i5 i30)))
(assert (not (= i5 i29)))
(assert (not (= i5 i28)))
(assert (not (= i5 i27)))
(assert (not (= i5 i26)))
(assert (not (= i5 i25)))
(assert (not (= i5 i24)))
(assert (not (= i5 i23)))
(assert (not (= i5 i22)))
(assert (not (= i5 i21)))
(assert (not (= i5 i20)))
(assert (not (= i5 i19)))
(assert (not (= i5 i18)))
(assert (not (= i5 i17)))
(assert (not (= i5 i16)))
(assert (not (= i5 i15)))
(assert (not (= i5 i14)))
(assert (not (= i5 i13)))
(assert (not (= i5 i12)))
(assert (not (= i5 i11)))
(assert (not (= i5 i10)))
(assert (not (= i5 i9)))
(assert (not (= i5 i8)))
(assert (not (= i5 i7)))
(assert (not (= i5 i6)))
(assert (not (= i4 i50)))
(assert (not (= i4 i49)))
(assert (not (= i4 i48)))
(assert (not (= i4 i47)))
(assert (not (= i4 i46)))
(assert (not (= i4 i45)))
(assert (not (= i4 i44)))
(assert (not (= i4 i43)))
(assert (not (= i4 i42)))
(assert (not (= i4 i41)))
(assert (not (= i4 i40)))
(assert (not (= i4 i39)))
(assert (not (= i4 i38)))
(assert (not (= i4 i37)))
(assert (not (= i4 i36)))
(assert (not (= i4 i35)))
(assert (not (= i4 i34)))
(assert (not (= i4 i33)))
(assert (not (= i4 i32)))
(assert (not (= i4 i31)))
(assert (not (= i4 i30)))
(assert (not (= i4 i29)))
(assert (not (= i4 i28)))
(assert (not (= i4 i27)))
(assert (not (= i4 i26)))
(assert (not (= i4 i25)))
(assert (not (= i4 i24)))
(assert (not (= i4 i23)))
(assert (not (= i4 i22)))
(assert (not (= i4 i21)))
(assert (not (= i4 i20)))
(assert (not (= i4 i19)))
(assert (not (= i4 i18)))
(assert (not (= i4 i17)))
(assert (not (= i4 i16)))
(assert (not (= i4 i15)))
(assert (not (= i4 i14)))
(assert (not (= i4 i13)))
(assert (not (= i4 i12)))
(assert (not (= i4 i11)))
(assert (not (= i4 i10)))
(assert (not (= i4 i9)))
(assert (not (= i4 i8)))
(assert (not (= i4 i7)))
(assert (not (= i4 i6)))
(assert (not (= i4 i5)))
(assert (not (= i3 i50)))
(assert (not (= i3 i49)))
(assert (not (= i3 i48)))
(assert (not (= i3 i47)))
(assert (not (= i3 i46)))
(assert (not (= i3 i45)))
(assert (not (= i3 i44)))
(assert (not (= i3 i43)))
(assert (not (= i3 i42)))
(assert (not (= i3 i41)))
(assert (not (= i3 i40)))
(assert (not (= i3 i39)))
(assert (not (= i3 i38)))
(assert (not (= i3 i37)))
(assert (not (= i3 i36)))
(assert (not (= i3 i35)))
(assert (not (= i3 i34)))
(assert (not (= i3 i33)))
(assert (not (= i3 i32)))
(assert (not (= i3 i31)))
(assert (not (= i3 i30)))
(assert (not (= i3 i29)))
(assert (not (= i3 i28)))
(assert (not (= i3 i27)))
(assert (not (= i3 i26)))
(assert (not (= i3 i25)))
(assert (not (= i3 i24)))
(assert (not (= i3 i23)))
(assert (not (= i3 i22)))
(assert (not (= i3 i21)))
(assert (not (= i3 i20)))
(assert (not (= i3 i19)))
(assert (not (= i3 i18)))
(assert (not (= i3 i17)))
(assert (not (= i3 i16)))
(assert (not (= i3 i15)))
(assert (not (= i3 i14)))
(assert (not (= i3 i13)))
(assert (not (= i3 i12)))
(assert (not (= i3 i11)))
(assert (not (= i3 i10)))
(assert (not (= i3 i9)))
(assert (not (= i3 i8)))
(assert (not (= i3 i7)))
(assert (not (= i3 i6)))
(assert (not (= i3 i5)))
(assert (not (= i3 i4)))
(assert (not (= i2 i50)))
(assert (not (= i2 i49)))
(assert (not (= i2 i48)))
(assert (not (= i2 i47)))
(assert (not (= i2 i46)))
(assert (not (= i2 i45)))
(assert (not (= i2 i44)))
(assert (not (= i2 i43)))
(assert (not (= i2 i42)))
(assert (not (= i2 i41)))
(assert (not (= i2 i40)))
(assert (not (= i2 i39)))
(assert (not (= i2 i38)))
(assert (not (= i2 i37)))
(assert (not (= i2 i36)))
(assert (not (= i2 i35)))
(assert (not (= i2 i34)))
(assert (not (= i2 i33)))
(assert (not (= i2 i32)))
(assert (not (= i2 i31)))
(assert (not (= i2 i30)))
(assert (not (= i2 i29)))
(assert (not (= i2 i28)))
(assert (not (= i2 i27)))
(assert (not (= i2 i26)))
(assert (not (= i2 i25)))
(assert (not (= i2 i24)))
(assert (not (= i2 i23)))
(assert (not (= i2 i22)))
(assert (not (= i2 i21)))
(assert (not (= i2 i20)))
(assert (not (= i2 i19)))
(assert (not (= i2 i18)))
(assert (not (= i2 i17)))
(assert (not (= i2 i16)))
(assert (not (= i2 i15)))
(assert (not (= i2 i14)))
(assert (not (= i2 i13)))
(assert (not (= i2 i12)))
(assert (not (= i2 i11)))
(assert (not (= i2 i10)))
(assert (not (= i2 i9)))
(assert (not (= i2 i8)))
(assert (not (= i2 i7)))
(assert (not (= i2 i6)))
(assert (not (= i2 i5)))
(assert (not (= i2 i4)))
(assert (not (= i2 i3)))
(assert (not (= i1 i50)))
(assert (not (= i1 i49)))
(assert (not (= i1 i48)))
(assert (not (= i1 i47)))
(assert (not (= i1 i46)))
(assert (not (= i1 i45)))
(assert (not (= i1 i44)))
(assert (not (= i1 i43)))
(assert (not (= i1 i42)))
(assert (not (= i1 i41)))
(assert (not (= i1 i40)))
(assert (not (= i1 i39)))
(assert (not (= i1 i38)))
(assert (not (= i1 i37)))
(assert (not (= i1 i36)))
(assert (not (= i1 i35)))
(assert (not (= i1 i34)))
(assert (not (= i1 i33)))
(assert (not (= i1 i32)))
(assert (not (= i1 i31)))
(assert (not (= i1 i30)))
(assert (not (= i1 i29)))
(assert (not (= i1 i28)))
(assert (not (= i1 i27)))
(assert (not (= i1 i26)))
(assert (not (= i1 i25)))
(assert (not (= i1 i24)))
(assert (not (= i1 i23)))
(assert (not (= i1 i22)))
(assert (not (= i1 i21)))
(assert (not (= i1 i20)))
(assert (not (= i1 i19)))
(assert (not (= i1 i18)))
(assert (not (= i1 i17)))
(assert (not (= i1 i16)))
(assert (not (= i1 i15)))
(assert (not (= i1 i14)))
(assert (not (= i1 i13)))
(assert (not (= i1 i12)))
(assert (not (= i1 i11)))
(assert (not (= i1 i10)))
(assert (not (= i1 i9)))
(assert (not (= i1 i8)))
(assert (not (= i1 i7)))
(assert (not (= i1 i6)))
(assert (not (= i1 i5)))
(assert (not (= i1 i4)))
(assert (not (= i1 i3)))
(assert (not (= i1 i2)))
(assert (let ((?v_0 (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) i11 e11) i12 e12) i13 e13) i14 e14) i15 e15) i16 e16) i17 e17) i18 e18) i19 e19) i20 e20) i21 e21) i22 e22) i23 e23) i24 e24) i25 e25) i26 e26) i27 e27) i28 e28) i29 e29) i30 e30) i31 e31) i32 e32) i33 e33) i34 e34) i35 e35) i36 e36) i37 e37) i38 e38) i39 e39) i40 e40) i41 e41) i42 e42) i43 e43) i44 e44) i45 e45) i46 e46) i47 e47) i48 e48) i49 e49) i50 e50)) (?v_1 (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 i46 e46) i9 e9) i1 e1) i41 e41) i17 e17) i11 e11) i7 e7) i22 e22) i23 e23) i25 e25) i24 e24) i31 e31) i34 e34) i13 e13) i43 e43) i49 e49) i19 e19) i3 e3) i29 e29) i33 e33) i48 e48) i8 e8) i16 e16) i39 e39) i38 e38) i5 e5) i12 e12) i47 e47) i37 e37) i28 e28) i26 e26) i10 e10) i50 e50) i6 e6) i4 e4) i15 e15) i14 e14) i30 e30) i35 e35) i18 e18) i42 e42) i20 e20) i32 e32) i27 e27) i21 e21) i36 e36) i2 e2) i44 e44) i40 e40) i45 e45))) (let ((?v_2 (sk ?v_0 ?v_1))) (not (= (select ?v_0 ?v_2) (select ?v_1 ?v_2))))))
(check-sat)
(exit)
